COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.require "memo.pub[let,jmc]" source
C00005 ENDMK
C⊗;
.require "memo.pub[let,jmc]" source
.at "qF" ⊂"%AF%*"⊃
.turn on "α"
.begin turn on "←→"; nofill;
CS258←Tying up a loose End→Winter 1979

.end

	The following theorem ties up a loose end from the lecture
of 13 February.

Theorem - Let ⊗D be partial ordered by <, and let < satisfy a
descending chain condition, i.e. admit a course-of-values induction
schema.  Let %2h:_D_→_D%1 and let the function g satisfy %2g:_D_→_D%1, 
%2(∀x)(¬(x_ε_D)_⊃_¬(g(x)_ε_D)%1 and %2(∀x)(x_ε_D_⊃_g(x)_>_x)%1.
Let the function ⊗f satisfy %2(∀x)(x_ε_D_⊃_f(x)_=_g(f(h(x))))%1.
Then %2(∀x)(x_ε_D_⊃_¬(f(x)_ε_D))%1.

Proof - The course-of-values induction schema is

	%2(∀x)(x ε D ∧ (∀y)(y ε D ∧ y < x ⊃ qF(y)) ⊃ qF(x))
⊃ (∀x)(x ε D ⊃ qF(x))%1.

In that schema we take

	%2qF(x) ≡ (∀z)(z ε D ⊃ f(z) ≠ x)%1.

Now choose %2x_ε_D%1, and suppose %2f(z)_=_x%1 for some %2z_ε_D%1.  We
then have

	%2x = f(z) = g(f(h(z))) > f(h(z))%1,

and so by the induction hypothesis, %2¬(f(h(z)) ε D)%1.
Hence by the properties of ⊗g,

	%2x = g(f(h(z)))%1

isn't in ⊗D either, which completes the induction. %81%1.

	The theorem shows the obvious facts that neither

.turn on "↑"
%2P1:	%2f(x) ← f(x↑2 + 1) + 1%1

nor

%2P2:	%2f(x) ← %1A%2.f(x.%1A%2)%1

terminates.  Of course, the minimization schema does it more simply,
but the theorem gives the further fact that the functional equations
have no solutions taking values among the natural numbers or S-expressions
respectively.